A Learning Based Approach to Control Synthesis of Markov Decision Processes for Linear Temporal Logic Specifications

摘要

We propose to synthesize a control policy for a Markov decision process (MDP)such that the resulting traces of the MDP satisfy a linear temporal logic (LTL)property. We construct a product MDP that incorporates a deterministic Rabinautomaton generated from the desired LTL property. The reward function of theproduct MDP is defined from the acceptance condition of the Rabin automaton.This construction allows us to apply techniques from learning theory to theproblem of synthesis for LTL specifications even when the transitionprobabilities are not known a priori. We prove that our method is guaranteed tofind a controller that satisfies the LTL property with probability one if sucha policy exists, and we suggest empirically with a case study in trafficcontrol that our method produces reasonable control strategies even when theLTL property cannot be satisfied with probability one.